Description

This PR allows function invocations to be on the LHS of mappings (instead of just variables).
This works by using the function string representation as a key in the variable resolver map, meaning they behave as if they were variables.
For example, func(a) == func(b) && func(b) == 1 → func(a) == 1.

Example

Before

State Refinement Error: Expected state size(stack²⁹⁵) > 0 but found size(stack²⁹⁵) == size(stack²⁹⁴) - 1 && size(stack²⁹⁴) == size(stack²⁹²) + 1 && size(stack²⁹²) == 0

After

State Refinement Error: Expected state size(stack²⁹⁴) > 0 but found size(stack²⁹⁴) == 0

Related Issue

None.

Type of change

• Bug fix
• New feature
• Documentation update
• Code refactoring

Checklist

• Added tests in ExpressionSimplifierTest
• mvn test passes locally
• Updated docs/README if behavior or API changed